($\lambda$$A$,${\it as}$,$i$,$z$. nth\_tl($i$;${\it as}$)) $\in$ $A$:Type$\rightarrow$($A$ List)$\rightarrow\mathbb{Z}\rightarrow\downarrow$True$\rightarrow$($A$ List)